Nuprl Definition : comp-atom-ap 0,22

comp-atom-ap(g;f;x;a)
== let f' = a.g o f in 
== let x' = a.x in 
== let F = b,cf'(b,x'(c)) in 
== let L = atoms-in(F) in 
== let b = new-atom((a.L)) in 
== if F(b,a)=aAtom inr(f'(b))
== iF(a,b)=aAtom inl(f.g(f(x'(b))))
== else inr(x.hd(list-diff(AtomDeq;monitor((f'(b,x)));b.L))) fi 
latex


Definitionsf o g, let x = a in b(x), if b t else f fi, x=yAtom, inl(x), inr(x), x.A(x), hd(l), list-diff(eq;as;bs), AtomDeq, f(a), car.cdr
FDL editor aliasescomp-atom-ap

origin